Recursion Schemes

再帰関数の再帰構造だけを抜き出して抽象化した概念。例えばRecursion Schemesの一つであるcataはリストにおけるfoldrトリックの一般化と言える。このように再帰関数から再帰構造を独立させることは法則を使った等式論証を可能にしたりコンパイラによる最適化を期待することが出来る。再帰を直接使わずにRecursion Schemesを使ってプログラムを書くことは、gotoを使わずにfor, whileを用いることで構造的なプログラムを書くことに例えることもできる。ある関手Fの始代数/終余代数として定義される代数的データ型からは、その始対象/終対象としての性質から別の(余)代数との間にユニークに伸びる射が存在する。この射を利用してRecursion Shemesは定義される。Recursion SchemesはSquiggolやBird–Meertens formalism (BMF) と呼ばれる、プログラム（特にリスト）が満たすべき仕様から等式論証によってプログラムの性質を導き出す計算手法が発展してできた分野である。

いちいちXXXmorphismと書くのは面倒なので以降ではmorphismを省略した関数名を使用する（見出しを除く）。例えばCatamorphismはcataと記載することにする。

Recursion Schemesを実装したHaskellのライブラリとしてはrecursion-schemesが有名。以降recursion-schemesと書いた場合はこのライブラリのことを指すこととする。

Catamorphism

F始代数から別のF代数に唯一伸びる射。リストにおけるfoldrの一般化。cata f は (|f|) とも書かれる。κατάはギリシャ語の前置詞で「下に、下へ」といった意味を指す（例：catastrophe）。

https://gyazo.com/1806cd7522f47b229ecdb93f17b6aa85

code:hs

-- | fの不動点を表す型

newtype Fix f = In { out :: f (Fix f) }

cata :: Functor f => (f a -> a) -> Fix f -> a

cata f = f . fmap (cata f) . out

cataの実装として以下のような書き方もある。

code:hs

cata f = c where c = f . fmap c . out

この書式は関数をinline化するのに適している（参考: Inline recursive functions using a wrapper）。

法則

code:hs

-- | Cata Eval, Cata Cancel

cata f . In == f . fmap (cata f)

-- | Cata Refl

cata In == id

-- | Cata Fusion

f . g == h . fmap f

=> f . cata g == cata h

-- | Cata Compose

eps :: forall x. f x -> g x

=> cata f . cata (In . eps) == cata (f . eps)

Example

code:hs

-- | 自然数の基礎となるデータ型

data NatF r = Z | S r deriving Functor

type Nat = Fix NatF

-- | Nat から Int への変換

toInt :: Nat -> Int

toInt = cata $ \case

Z -> 0

S n -> n + 1

-- | Natにおける0

zero :: Nat

zero = In Z

-- | Natにおける後者関数（+1）

succ :: Nat -> Nat

succ n = In (S n)

-- | 足し算

add :: Nat -> Nat -> Nat

add n = cata $ \case

Z -> n

S m -> succ m

-- | 掛け算

mul :: Nat -> Nat -> Nat

mul n = cata $ \case

Z -> zero

S r -> n add r

参考文献

E. Meijer, M.M. Fokkinga, and R. Paterson. "Functional programming with bananas, lenses, envelopes and barbed wire." 1991

Anamorphism

F終余代数に別ののF余代数から唯一伸びる射。リストにおけるunfoldrの一般化。ana f は [(f)] とも書かれる。ἀνάはギリシャ語の前置詞で「上に、上へ」といった意味を指す（例：anabolism）。

https://gyazo.com/ae6a313ced4e08698c57cf60761e03d1

code:hs

ana :: Functor f => (a -> f a) -> a -> Fix f

ana f = In . fmap (ana f) . f

法則

code:hs

-- | Ana Eval

out . ana f == fmap (ana f) . f

-- | Ana UP (Uniqueness Property)

out . g = fmap g . f

=> g == ana f

-- | Ana Fusion

f . g == fmap g . h

=> ana f . g == ana h

Example

code:hs

-- | Int から Nat への変換

fromInt :: Int -> Nat

fromInt = ana $ \n ->

if n == 0 then Z else S (n-1)

参考文献

E. Meijer, M.M. Fokkinga, and R. Paterson. "Functional programming with bananas, lenses, envelopes and barbed wire." 1991

Hylomorphism

anaとcataをこの順に組み合わせることで、再帰的な中間構造を生成する関数を実装できるようにしたもの。hylo f gは[| f, g |] とも書かれる。ὑλο- (< ὕλη) はギリシャ語で「木材、材質」を表し、アリストテレス哲学においては質料を表す。

https://gyazo.com/8d6418dde5edfd5fdbe610b4a941be1a

code:hs

hylo :: Functor f => (f b -> b) -> (a -> f a) -> a -> b

hylo f g = f . fmap (hylo f g) . g

法則

code:hs

-- | Hylo Split

hylo f g = cata f . ana g

-- | Hylo Shift

hylo (f . h) g = hylo f (g . h)

-- | Hylo Fusion (Left)

f . g == g' . fmap f

=> f . hylo g h == hylo g' h

-- | Hylo Fusion (Right)

h . f == fmap f . h'

=> hylo g h . f == hylo g h'

Example

code:hs

-- | リストの基礎となるデータ型

data ListF a r = Nil | Cons a r deriving Functor

type List a = Fix (ListF a)

-- | 階乗を求める関数

-- anaを使ってnを1..nに展開したあとにcataを使ってリスト全体の積を計算している

fact :: Int -> Int

fact = hylo f g

where

f Nil = 1

f (Cons a r) = a * r

g n = if n == 0 then Nil else Cons n (n-1)

参考文献

E. Meijer, M.M. Fokkinga, and R. Paterson. "Functional programming with bananas, lenses, envelopes and barbed wire." 1991

Fix と Base t

ListFとListのようにFixを使って型を定義する方針だと既存のリストの型[a]が使えないという難点がある。これを解決するために、型族と型クラスを用いて既存の型からそれを不動点として表すような型との関係を定義する方法がある。

code:hs

-- | リストの基礎となるデータ型

data ListF a r = Nil | Cons a r deriving Functor

-- | 関手の不動点として表されるデータ構造とその基礎となる関手を関係づける型族

type family Base t :: * -> *

type instance Base a = ListF a

-- | 再帰のRecursion Schemes

class Functor (Base t) => Recursive t where

project :: t -> Base t t

-- | Catamorphism

cata :: (Base t a -> a) -> t -> a

cata f = f . fmap (cata f) . project

-- | リストの再帰構造

instance Recursive a where

project [] = Nil

project (x:xs) = Cons x xs

これを使えば例えばリストの長さを計算する関数length' は以下のように実装することが出来る。

code:hs

length' :: a -> Int

length' = cata $ \case

Nil -> 0

(Cons _ r) -> r + 1

Folds/Unfolds/Refolds

cata, ana, hyloは最も基本的なRecursion Schemesであるが、その能力に制限があるため様々な改良が施されたRecursion Schemesが開発されている。これらはデータ型から伸びる関数の向きに特徴があるため、それぞれの向きを持つRecursion SchemesをFolds, Unfolds, Refoldsと名前をつけて分類する。

https://gyazo.com/f0a41ff971a313621af4fbfd27a4a39a

画像元: https://github.com/sellout/recursion-scheme-talk/blob/master/cheat%20sheet.pdf

Folds

Paramorphism

cataの引数を参照できないという制約を改良したRecursion Schemes。para fは[< f >]とも書かれる。παράはギリシャ語の前置詞で「…に沿って、…の側に、…の側へ」という意味。

https://gyazo.com/fc80ccde9a6e64276861fd6e075f9d53

code:hs

para :: Functor f => (f (Fix f, a) -> a) -> Fix f -> a

para f = f . fmap ((,) <*> para f) . out

法則

code:hs

-- | Para Eval

para f . In == f . (\x -> fmap ((x,) . para f)

-- | Para Fusion

f . g == h . fmap (\(x, r) -> (x, f r))

=> f . para g = para h

Example

code:hs

-- | Nat における1

one :: Nat

one = succ zero

-- | 階乗

fact :: Nat -> Nat

fact = para $ \case

Z -> one

S (n, r) -> (succ n) mul r

参考文献

Lambert Meertens "Paramorphisms" 1990

E. Meijer, M.M. Fokkinga, and R. Paterson. "Functional programming with bananas, lenses, envelopes and barbed wire." 1991

Zygomorphism

cataで再帰的な計算を行う際に別の値も同時に計算できるように拡張したもの。paraの一般化とみなせる。

https://gyazo.com/8ff3315ee0dcc2c15acfc1290947b259

code:hs

zygo :: Functor f => (f b -> b) -> (f (b, a) -> a) -> Fix f -> a

zygo f g = snd . cata (\x -> (f (fmap fst x), g x))

$ Bを$ \mu Fと置き$ fを$ in とすれば zygo In となり、これはpara と一致する。

Example

Functional Pearl: Maximally Dense Segments

参考文献

G. R. Malcolm and Rijksuniversiteit te Groningen "Algebraic data types and program transformation" 1990

Mutumorphism

相互再帰を実現するRecursion Schemes。zygoの一般化と考えることも出来る。

code:hs

mutu :: Functor f => (f (a, b) -> a) -> (f (a, b) -> b) -> Fix f -> (a, b)

mutu f g = cata (\x -> (f x, g x))

参考文献

Martinus Maria Fokkinga "Law and Order in Algorithmics" 1992

para, zygo, mutuの関係

mutuの特別な場合はzygoであり、zygoの特別な場合がparaとなる。コードで表すと以下のようになる。

code:hs

-- zygoからparaを導出する

para == zygo In

-- mutuからzygoを導出する

zygo f g == snd . mutu (f . fmap fst) g

Histomorphism

全ての過去の計算結果にアクセスできるようなcata。

code:hs

data Cofree f a = a :< f (Cofree f a)

extract :: Cofree f a -> a

extract (a :< _) = a

histo :: Functor f => (f (Cofree f a) -> a) -> Fix f -> a

histo f = extract . cata (\x -> f x :< x)

Example

code:hs

-- | フィボナッチ数列

fibo :: Nat -> Nat

fibo = histo $ \case

Z -> one

S (_ :< Z) -> one

S (a :< S (b :< _)) -> a add b

参考文献

Tarmo UUSTALU and Varmo VENE "Primitive (Co)Recursion and Course-of-Value (Co)Iteration, Categorically" 1999

Prepromorphism

cataで畳み込む際に自然変換で表現される前処理(preprocessing) を伴うようなRecursion Schemes。

code: hs

prepro :: Functor f => (forall a. f a -> f a) -> (f a -> a) -> Fix f -> a

prepro h f = f . fmap (prepro h f . cata (In . h)) . out

参考文献

Martinus Maria Fokkinga "Law and Order in Algorithmics" 1992

Unfolds

Apomorphism

paraの圏論的な双対。anaと同様に再帰的なデータを構築できるが、apoはその途中で残りの再帰的なデータ型を直接返すことが出来るようになっている。απόはギリシャ語の前置詞で「…を離れて、…から」という意味。

https://gyazo.com/954dacb833042064f9d971241bea6971

code:hs

apo :: Functor f => (a -> f (Either (Fix f) a)) -> a -> Fix f

apo f = In . (fmap (either id (apo f))) . f

参考文献

Varmo Vene and Tarmo Uustalu "Functional Programming with Apomorphisms / Corecursion" 1998

Futumorphism

再帰的なデータ型を構築する際に任意個先の計算結果まで計算することが出来るようなRecursion Schemes。

code:hs

data Free f a = Pure a | Free (f (Free f a))

futu :: Functor f => (a -> f (Free f a)) -> a -> Fix f

futu f = ana g . Pure where

g (Pure a) = f a

g (Free fm) = fm

参考文献

Tarmo UUSTALU and Varmo VENE "Primitive (Co)Recursion and Course-of-Value (Co)Iteration, Categorically" 1999

Postpromorphism

anaで再帰的なデータを構築する際に自然変換で表現される後処理(postprocessing) を伴うようなRecursion Schemes。

code:hs

postpro :: Functor f => (forall f a -> f a) -> (a -> f a) -> a -> Fix f

postpro h f = In . fmap (ana (h . out) . postpro h f) . f

参考文献

Martinus Maria Fokkinga "Law and Order in Algorithmics" 1992

Refolds

Metamorphism

hyloのanaとcataの合成の順番を逆にして再帰的なデータ型から再帰的なデータ型への変換を実現するようなRecursion schemes。Metamorphismと名前がつくRecursion SchemesはErwigによるものとGibbonsによるものとの2種類が存在する。

code:hs

-- | Jeremy Gibbons' metamorphism

meta :: (Functor f, Functor g) => (f a -> a) -> (a -> b) -> (b -> g b) -> Fix f -> Fix g

meta f g h = ana h . g . cata f

参考文献

Martin Erwig "Metamorphic Programming: Structured Recursion for Abstract Data Types" 1998

Jeremy Gibbons "Metamorphisms: Streaming Representation-Changers" 2005

Chronomorphism

histoとfutuを組み合わせたようなRecursion Schemes。

code:hs

chrono :: Functor f => (f (Cofree f b) -> b) -> (a -> f (Free f a)) -> a -> b

chrono f g = histo f . futu g

自由度は非常に高いがchronoの力が必要な実例はまだ見つかっていない様子。

Sadly, I have no practical examples of a chronomorphism. I didn't find that to be a very productive t..

https://twitter.com/kmett/status/318410115101380608

参考文献

Edward Kmett "Time for Chronomorphisms" 2008

Dynamorphism

histoは過去のすべての計算を参照することが出来るので動的計画法のような計算結果を再利用するようなアルゴリズムを実装するために使えるが、計算結果のデータ構造が入力のデータ構造と同じものに制限されるという制約があった。そこで予めanaで適切なデータ型の値に展開した後にhistoを使って計算するというdynaが考案された。

code:hs

dyna :: Functor f => (f (Cofree f b) -> b) -> (a -> f a) -> a -> b

dyna phi psi = extract . hylo ap psi

where ap f = phi f :< f

参考文献

Jevgeni Kabanov and Varmo Vene "Recursion Schemes for Dynamic Programming" 2006

Ralf Hinze and Nicolas Wu "Histo- and Dynamorphisms Revisited" 2013

Elgot algebra

再帰的にデータを展開する途中でcataで畳み込む時の値を返すような短絡評価が行えるRecursion Schemes。

code:hs

elgot :: Functor f => (f b -> b) -> (a -> Either b (f a)) -> a -> b

elgot f g = either id (f . fmap (elgot f g)) . g

参考文献

Jiri Adamek, Stefan Milius, Jiri Velebil "Elgot Algebras" 2006

The Comonad.Reader » Elgot (Co)Algebras

Monadic Recursion Schemes

F代数をモナドMのクライスリ圏で考えることによって副作用を伴うRecursion Schemesを考えることが出来る。ただしFとMの間には適切な分配法則が定められている必要がある。これはHaskellではFにFunctorよりも強い制約を要求することになる。

例えば副作用を伴うcataであるcataMは以下のように実装することが出来る。

https://gyazo.com/2f8b30bfb2e2fe93fa221777a3cd2a92

code:hs

cataM :: (Traversable f, Monad m) => (f a -> m a) -> Fix f -> m a

cataM = cata . (sequence >=>)

実装は Suggestion: Add monadic variants of various ...morphism functions. #3 を参考。

参考文献

Maarten Fokkinga "Monadic Maps and Folds for Arbitrary Datatypes" 1994

Erik Meijer and Johan Jeuring "Merging Monads and Folds for Functional Programming" 1995

Mendler style

Coyonedaを用いることで再帰的な型を計算するMendler StyleのRecursion Schemesを考えることが出来る。

code:hs

mcata :: (forall b. (b -> a) -> f b -> a) -> Fix f -> a

mcata f = f (mcata f) . out

mcataではfに対してFunctorのインスタンスであることが要請されていないことに注意。Mendler styleのRecursion Schemesを利用することでより一般的なデータ型のRecursion Schemesを考えることが出来る。

mcataを使ってcataは以下のように導出できる。

code:hs

cata :: Functor f => (f a -> a) -> Fix f -> a

cata f = mcata (\g -> f . fmap g)

参考: Catamorphisms#Mendler Style - School of Haskell

またMendler styleでのHistomorphismの実装はCofreeのような中間構造が必要ないというメリットがある。

code:hs

mhisto :: (forall y. (y -> c) -> (y -> f y) -> f y -> c) -> Fix f -> c

mhisto psi = psi (mhisto psi) out . out

参考文献

Tarmo UUSTALU and Varmo VENE "MENDLER-STYLE INDUCTIVE TYPES, CATEGORICALLY" 1999

Tarmo Uustalu and Varmo Vene "Coding Recursion a la Mendler" 2000

一般化

目的に応じてアドホックに作られ種類が多く存在するRcursion Schemesだが、抽象的な定義を用いることで統一的な見方

を与える方法も存在する。

Recursion Schemes from Comonads

再帰的な処理の際に値を引き回す構造を適当な分配法則を持つコモナドで表現することによってcata, para, zygo, histo等のRecursion Schemesを統合することが出来る。

https://gyazo.com/faae86c8a5f670bae6b41a0d4a9a8447

code:hs

gcata :: (Functor f, Comonad w) => (forall b. f (w b) -> w (f b)) -> (f (w a) -> a) -> Fix f -> a

gcata dist f = extract . c where c = fmap f . dist . fmap (duplicate . c) . out

cata

コモナドとして恒等関手を採用すると単純なcataになる。

code:hs

distCata :: Functor f => f (Identity a) -> Identity (f a)

distCata = Identity . fmap runIdentity

cata :: Functor f => (f (Identity a) -> a) -> Fix f -> a

cata = gcata distCata

zygo

コモナドとして別の型との積 $ B \times - を採用するとzygoになる。

code:hs

distZygo :: Functor f => (f b -> b) -> f (b, a) -> (b, f a)

distZygo g m = (g (fmap fst m), fmap snd m)

zygo :: Functor f => (f b -> b) -> (f (b, a) -> a) -> Fix f -> a

zygo g = gcata (distZygo g)

paraはzygoの特殊な場合であった。この場合gとしてInを採用するとparaを実装することも出来る。

histo

コモナドとしてCofreeを採用するとhistoになる。

code:hs

distHisto :: Functor f => f (Cofree f a) -> Cofree f (f a)

distHisto fc = fmap extract fc :< fmap (\(_ :< fc') -> distHisto fc') fc

histo :: Functor f => (f (Cofree f a) -> a) -> Fix f -> a

histo = gcata distHisto

参考文献

TARMO UUSTALU, VARMO VENE and ALBERTO PARDO "RECURSION SCHEMES FROM COMONADS" 2001

Adjoint folds and unfolds

随伴の関係にある関手$ L \dashv R, L: {\mathscr C} \rightarrow {\mathscr D}, R: {\mathscr D} \rightarrow {\mathscr C}と自己関手 $ C: {\mathscr C} \rightarrow {\mathscr C}, D: {\mathscr D} \rightarrow {\mathscr D}、そして分配法則 $ \sigma: L\circ D \rightarrow C\circ Lが与えられた時、

https://gyazo.com/fb79abf83d3eef00be7b795fe2857fd2

$ a : CA \rightarrow A に対して adjoin fold を$ x \cdot L\ in = a \cdot Cx \cdot \sigma_{\mu D} を満たす唯一の射として定義する。すなわち$ xは以下の図式を可換にする唯一の射である（唯一性は随伴 $ L \dashv Rを利用して証明される）。

https://gyazo.com/3fc3b7ac4c113e75bdd2d1311f5571e4

$ L \dashv Rとして忘却関手とコモナドの随伴を考えることでadjoint foldsの考え方はRecursion Schemes from Comonadを含んでいることが分かる。

参考文献

Ralf Hinze "Adjoint Folds and Unfolds Or: Scything Through the Thicket of Morphisms" 2010

Ralf Hinze, Nicolas Wu and Jeremy Gibbons "Unifying Structured Recursion Schemes" 2013

応用

コンパイラによる最適化: 融合変換

TODO